p:FinProbSpace, n:, X, Y:RandomVariable(p;n).
rv-disjoint(p;n;X;Y)  (m:. (n  m)  rv-disjoint(p;m;X;Y)) 

latex

Definitions	x:A. B(x), P  Q, rv-disjoint(p;n;X;Y), t  T, {i..j}, i  j < k, P & Q, S  T, P  Q, , suptype(S; T), {T}, Top, , Outcome, A, A  B, Dec(P), False, FinProbSpace, RandomVariable(p;n)
Lemmas	decidable lt, int seg wf, le wf, nat wf, rv-disjoint wf, random-variable wf, finite-prob-space wf, p-outcome wf, not wf, rationals wf, top wf, subtype rel function, length wf nat, false wf